(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const r3 Real)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const r4 Real)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const r5 Real)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const r6 Real)
(declare-const v16 Bool)
(assert (or v16 v5 (> (/ 71.0 71.0) r3 0.0)))
(assert (or (> (/ 71.0 71.0) r3 0.0) (<= (- (* 71.0 71.0 4590495740.0 4590495740.0)) (/ 71.0 71.0)) (and v5 v1 v2 v6 v4 v4 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3))))
(assert (or (> (/ 71.0 71.0) r3 0.0) v5 v5))
(assert (or v5 (or v7 v5 (and v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6) v12 v3 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v9 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3) v3 v4 v2 (=> v10 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)))) v8 v0) v5))
(assert (or (<= (- (* 71.0 71.0 4590495740.0 4590495740.0)) (/ 71.0 71.0)) (not (distinct v5 (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6))) (distinct v5 (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6))))
(assert (or (> (/ 71.0 71.0) r3 0.0) (or v7 v5 (and v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6) v12 v3 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v9 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3) v3 v4 v2 (=> v10 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)))) v8 v0) (<= (- (* 71.0 71.0 4590495740.0 4590495740.0)) (/ 71.0 71.0))))
(assert (or (and v11 (> (* 71.0 71.0 4590495740.0 4590495740.0) (* 71.0 71.0 4590495740.0 4590495740.0) (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0) 4590495740.0) (or v7 v5 (and v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6) v12 v3 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v9 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3) v3 v4 v2 (=> v10 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)))) v8 v0) (distinct (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v0 v10 (distinct (/ 71.0 71.0) (* 71.0 71.0 4590495740.0 4590495740.0) (/ 71.0 71.0) 71.0 71.0)) v4 (not v7) (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0))) (distinct v5 (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6)) (not (distinct v5 (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6)))))
(assert (or (distinct v5 (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6)) (and v5 v1 v2 v6 v4 v4 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3)) (or v7 v5 (and v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6) v12 v3 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v9 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3) v3 v4 v2 (=> v10 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)))) v8 v0)))
(assert (or (and v5 v1 v2 v6 v4 v4 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3)) (and v5 v1 v2 v6 v4 v4 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3)) (> (/ 71.0 71.0) r3 0.0)))
(assert (or (or v7 v5 (and v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6) v12 v3 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v9 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3) v3 v4 v2 (=> v10 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)))) v8 v0) v5 (not (distinct v5 (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6)))))
(assert (or (and v11 (> (* 71.0 71.0 4590495740.0 4590495740.0) (* 71.0 71.0 4590495740.0 4590495740.0) (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0) 4590495740.0) (or v7 v5 (and v8 (or v6 (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (<= 71.0 71.0 r3) v4 v5 v5 v6) v12 v3 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v9 (distinct v0 v1 v2 v0 v3 v2 v1 v4 v3) v3 v4 v2 (=> v10 (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)))) v8 v0) (distinct (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0)) (< 4590495740.0 (* r3 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0)) v0 v10 (distinct (/ 71.0 71.0) (* 71.0 71.0 4590495740.0 4590495740.0) (/ 71.0 71.0) 71.0 71.0)) v4 (not v7) (> 0.0 0.0 (* 71.0 71.0 4590495740.0 4590495740.0))) v5 v5))
(check-sat)
